A (strict) [[symmetric monoidal structure]] on a [[preorder]] $(X, \leq)$ consists of two constituents: - an element $I \in X$, called the [[monoidal unit]] - a function $\otimes: X \times X \rightarrow X$, called the [[monoidal product]] These constituents must satisfy the following properties, where we write $\otimes (x_1, x_2) = x_1 \otimes x_2$: - for all $x_1, x_2, y_1, y_2 \in X$, if $x_1 \leq y_1$ and $x_2 \leq y_2$, then $x_1 \otimes x_2 \leq y_1 \otimes y_2$ - for all $x \in X$, the equations $I \otimes x = x$ and $x \otimes I = x$ hold - for all $x, y, z \in X$, the equation $(x \otimes y) \otimes z = x \otimes (y \otimes z)$ holds - for all $x, y \in X$, the equation $x \otimes y = y \otimes x$ holds We call these conditions [[monotonicity]], [[unitality]], [[associativity]] and [[symmetry]] respectively. A [[preorder]] equipped with a [[symmetric monoidal structure]] $(X, \leq, I, \otimes)$ is called a [[symmetric monoidal structure|symmetric monoidal preorder]].